FDL - Nuprl Lemma : fpf-rename-dom

Nuprl Lemma : fpf-rename-dom

A, C:Type, B:(A

Type), eqa:EqDecider(A), eqc:EqDecider(C), r:(A

C), f:a:A fp

B(a), c:C.
c

dom(rename(r;f))

(

a:A. a

dom(f) & c = r(a))

Definitions x(s), EqDecider(T), rename(r;f), x dom(f), a:A fp B(a), x. t(x), map(f;as), deq-member(eq;x;L), b, x:A. B(x), t T, Prop, P Q, P & Q, P Q, P Q, x:A. B(x), A & B, (x l)

Lemmas member map, iff functionality wrt iff, l member wf, assert wf, deq-member wf, map wf, assert-deq-member, cand functionality wrt iff, exists functionality wrt iff, deq wf, fpf wf